∀E KW S,P,W;
∀E REFLEX S,W;
∀E KNOW S,NOT(P),W;
∀E NOT W,P;
ASSUME T(K(S,NOT(P)),W);
TAUT ∀W1.(A(S,W,W1)⊃T(NOT(P),W1)) ↑↑↑,↑;
∀E ↑ W;
⊃E 2,↑;
⊃I 5⊃↑;
TAUT (T(P,W)∧T(KW(S,P),W))⊃T(K(S,P),W) 1,4,↑;
LABEL KW1;
∀I ↑ S P W;
∀E KNOW S,P,W;
ASSUME T(K(S,P),W);
TAUT ∀W1.(A(S,W,W1)⊃T(P,W1)) ↑↑:↑;
∀E ↑ W;
⊃E 2,↑;
⊃I 13⊃↑;
LABEL KNOWTRUE;
∀I ↑ S P W;
∀E FOOL FOOL,P,W;
∀E FOOL S,K(FOOL,P),W;
∀E KNOWTRUE FOOL,K(S,K(FOOL,P)),W;
TAUT T(K(FOOL,P),W)⊃T(K(S,K(FOOL,P)),W) ↑↑↑:↑;
LABEL FOOLTRUE;
∀I ↑ S W P;
∀E KNOW S,K(FOOL,P),W;
ASSUME T(K(FOOL,P),W);
TAUT ∀W1.(A(S,W,W1)⊃T(K(FOOL,P),W1)) 22,↑↑:↑;
∀E ↑ W1;
⊃I ↑↑↑⊃↑;
TAUT (T(K(FOOL,P),W)∧A(S,W,W1))⊃T(K(FOOL,P),W1) ↑;
LABEL FOOLTRANS;
∀I ↑ S P W W1;